#!/usr/bin/python

import re
import os
import sys
debug = True

lines = sys.stdin.readlines()
lemma = sys.argv[1]

# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL


rank = []             # list of list of goals, main list is ordered by priority
maxPrio = 50
for i in range(0,maxPrio):
  rank.append([])


if lemma == "recentalive_tag":
  # only prioritize TagRun() and Tag() goals, otherwise standard auto
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    if re.match('.*TagRun\(.*', line):
      rank[40].append(num)
    elif re.match('.*Tag\(.*', line):
      rank[20].append(num)
    else:
      rank[5].append(num)

if lemma == "Observational_equivalence":
  # only prioritize TagRun() and Tag() goals, otherwise standard auto
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)

    if re.match('.*TagRun\(.*', line):
      rank[40].append(num)
    elif re.match('.*Tag\(.*', line):
      rank[20].append(num)
    else:
      rank[5].append(num)


elif lemma == "executable":
  # ???
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    #if re.match('.*Update\(.*', line):
    #  rank[0].append(num)
    #else:
    rank[5].append(num)


else:
  if debug:
    sys.stderr.write("No lemma found")
  exit(0)

# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
  for goal in listGoals:
    if debug:
      sys.stderr.write(goal)
      print goal

